$\forall$${\it es}$:ES. es\_init(${\it es}$) $\in$ $i$:Id$\rightarrow$state@$i$